es:ES, Cmd:Type, isupdate:(Cmd), In:AbsInterface(Cmd), Out:AbsInterface(Top),
Sys:AbsInterface(Cmd List).
(E(In) r E(Sys))
 (f:sys-antecedent(es;Sys).
 (u:E(Sys). (f(u) = u  E)  ((u  In)))
  fifo-antecedent(es;Sys;f)
  input-forwarding{i:l}
  input-forwarding(es; Cmd; Sys; isupdate; In; f)
  (chain:(E(Sys)(Id List)).
  chain-consistent(f;chain)
   (e:E(Sys).
   filter(isupdate;es-interface-history(es; Sys; e))
   =
   In(updates(cr-explanation{i:l}
   In(updates(cr-explanation(es; Sys; f; e)))
    (Cmd List)))) 

latex

Up	abstract chain replication
Definitions	bounded-input-forwarding{i:l}(es; Cmd; Sys; isupdate; In; f; b)  {FDLNOr1385}, x:AB(x), x:A. B(x), s = t, t  T, strong-subtype(A;B), P  Q, ES, Type, AbsInterface(A), sys-antecedent(es;Sys), fifo-antecedent(es;Sys;f), input-forwarding{i:l}(es; Cmd; Sys; isupdate; In; f), chain-consistent(f;chain), E(X), x:A  B(x), b, , left + right, {x:A| B(x)} , if b then t else f fi , P & Q, P  Q, P  Q, P  Q, e loc e' , x:A. B(x), did-forward(es; Sys; f; e), type List, a < b, A, hd(l), L1  L2, adjacent(T;L;x;y), (x  l), no_repeats(T;l), Top, cr-explanation{i:l}(es; Sys; f; e), updates(L), X(L), es-interface-history(es; X; e), filter(P;l), Id, e  X, f(a), E, should-forward(es; In; isupdate; f; a), (e <loc e'), [], X(e), loc(e), [car / cdr], e c e', <a, b>, !Void(), x:A.B(x), f(x)?z, a:A fp B(a), , let x,y = A in B(x;y), t.1, Unit, ff, inr x , tt, inl x , False, True, case b of inl(x) => s(x) | inr(y) => t(y), EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd, x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, constant_function(f;A;B), A  B, i  j , ||as||, last(L), , Outcome, #$n, x  dom(f), prior(X), nth_tl(n;as), Atom$n, (e < e'), A c B, a = b, x.A(x), T
Lemmas	squash wf, es-interface-history wf, filter wf, not functionality wrt iff, exists functionality wrt iff, and functionality wrt iff, assert-eq-id, eq id wf, es-causl wf, bounded-input-forwarding-invariant, updates of wf, es-interface-vals wf, no repeats wf, length wf1, l member wf, ifthenelse wf, es-interface-val wf2, hd wf, adjacent wf, last wf, sublist wf, chain-consistent wf, input-forwarding wf, es-loc wf, es-le wf, fifo-antecedent wf, rev implies wf, iff wf, constant function wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, IdLnk wf, deq wf, event system wf, es-E-interface-subtype rel, true wf, false wf, btrue wf, bfalse wf, unit wf, bool wf, es-is-interface wf, es-E wf, sys-antecedent wf, member wf, es-interface wf, es-interface-subtype rel, top wf, subtype rel wf, es-causle wf, should-forward wf, did-forward wf, es-locl wf, Id wf, not wf, assert wf, es-E-interface wf, bounded-input-forwarding_wf